from mythril.analysis import solver
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import DOS_WITH_BLOCK_GAS_LIMIT
from mythril.exceptions import UnsatError
from mythril.analysis.module.base import DetectionModule, EntryPoint
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.transaction.symbolic import ACTORS
from mythril.laser.smt.bool import And
from mythril.laser.smt import symbol_factory,UGT
from mythril.laser.ethereum.transaction.transaction_models import (
    ContractCreationTransaction,
)
from mythril.laser.ethereum.state.constraints import Constraints
import logging


log = logging.getLogger(__name__)

DESCRIPTION = """
GasValue
"""


class GasValue(DetectionModule):
    """This module checks GasValue"""

    name = "GasValue"
    swc_id = DOS_WITH_BLOCK_GAS_LIMIT
    description = DESCRIPTION
    entry_point = EntryPoint.CALLBACK
    pre_hooks = ["CALL"]

    def __init__(self):
        super().__init__()
        self._cache_address = {}

    def reset_module(self):
        """
        Resets the module
        :return:
        """
        super().reset_module()

    def _execute(self, state: GlobalState) -> None:
        """

        :param state:
        :return:
        """
        if state.get_current_instruction()["address"] in self.cache:
            return
        issues = self._analyze_state(state)
        for issue in issues:
            self.cache.add(issue.address)
        self.issues.extend(issues)

    @staticmethod
    def _analyze_state(state):
        instruction = state.get_current_instruction()
        description_head = "GasValue."
        
        op=state.environment.code.instruction_list[state.mstate.pc - 1]["opcode"]
        val=state.mstate.stack[-3]
        
        if op=="GAS" and val!= 0:
            try:
                transaction_sequence = solver.get_transaction_sequence(
                    state,
                    state.world_state.constraints
                )

                description_tail = (
                    "GasValue"
                )

            except UnsatError:
                transaction_sequence = solver.get_transaction_sequence(
                    state, state.world_state.constraints
                )
                description_tail = (
                    "GasValue false "
                )

            issue = Issue(
                contract=state.environment.active_account.contract_name,
                function_name=state.environment.active_function_name,
                address=instruction["address"],
                swc_id=DOS_WITH_BLOCK_GAS_LIMIT,
                bytecode=state.environment.code.bytecode,
                title="GasValue",
                severity="low",
                description_head=description_head,
                description_tail=description_tail,
                transaction_sequence=transaction_sequence,
                gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
            )
            return [issue]


        return []


detector = GasValue()
